PRISM
=====
Version: 4.5.dev
Date: Sat Mar 14 23:29:08 UTC 2020
Hostname: e72bdd194fc5
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -heuristic speed -e 1e-6 -maxiters 1000000 rabin.10.prism rabin.10.props --property live
Parsing model file "rabin.10.prism"...
Type: MDP
Modules: process1 process2 process3 process4 process5 process6 process7 process8 process9 process10
Variables: c b r p1 b1 r1 draw1 p2 b2 r2 draw2 p3 b3 r3 draw3 p4 b4 r4 draw4 p5 b5 r5 draw5 p6 b6 r6 draw6 p7 b7 r7 draw7 p8 b8 r8 draw8 p9 b9 r9 draw9 p10 b10 r10 draw10
Parsing properties file "rabin.10.props"...
1 property:
(1) "live": Pmax=? [ F (p1=2|p2=2|p3=2|p4=2|p5=2|p6=2|p7=2|p8=2|p9=2|p10=2) ]
---------------------------------------------------------------------
Model checking: "live": Pmax=? [ F (p1=2|p2=2|p3=2|p4=2|p5=2|p6=2|p7=2|p8=2|p9=2|p10=2) ]
Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).
Building model...
Computing reachable states...
Reachability (BFS): 42 iterations in 60.26 seconds (average 1.434643, setup 0.00)
Time for model construction: 65.047 seconds.
Type: MDP
States: 358055586147376 (1 initial)
Transitions: 2908346849726720
Choices: 696028935338720
Transition matrix: 894897 nodes (9 terminal), 2908346849726720 minterms, vars: 96r/96c/10nd
Warning: Switching to MTBDD engine, as number of states is too large for Sparse engine.
Prob0A: 5 iterations in 1.18 seconds (average 0.235400, setup 0.00)
Prob1E: 6 iterations in 0.67 seconds (average 0.112000, setup 0.00)
yes = 358055586147376, no = 0, maybe = 0
Value in the initial state: 1.0
Time for model checking: 1.913 seconds.
Result: 1.0 (value in the initial state)
Overall running time: 67.647 seconds.
---------------------------------------------------------------------
Note: There were 2 warnings during computation.